
; Copyright (c) 2015 Microsoft Corporation

; BUG: mpf != fpu [seed=1365672267, num_tests=55148]
; Rounding mode: to negative
; Precision: double (11/53)
; X = +1.743105131865309687100307201035320758819580078125p-885 [+ 3346647994965712 -885 N] {+ 3346647994965712 -885 (6.75737e-267)}
; Y = -1.9517798820926548497567409867770038545131683349609375p845 [- 4286435522331215 845 N] {- 4286435522331215 845 (-4.57907e+254)}
; Z = -1.8242957893466726915221443050540983676910400390625p-40 [- 3712298209744744 -40 N] {- 3712298209744744 -40 (-1.65919e-012)}
; +1.743105131865309687100307201035320758819580078125p-885 [+ 3346647994965712 -885 N] x -1.9517798820926548497567409867770038545131683349609375p845 [- 4286435522331215 845 N] -1.8242957893466726915221443050540983676910400390625p-40 [- 3712298209744744 -40 N] == -1.3066133295234620970148853302816860377788543701171875p-38 [- 1380863676588691 -38 N]
; [HW: -1.30661332952346231905949025531299412250518798828125p-38 [- 1380863676588692 -38 N]] 

; mpf : - 1380863676588691 -38
; mpfd: - 1380863676588691 -38 (-4.75343e-012) class: Neg. norm. non-zero
; hwf : - 1380863676588692 -38 (-4.75343e-012) class: Neg. norm. non-zero

(set-logic QF_FP)
(set-info :status unsat)

(define-sort FPN () (_ FloatingPoint 11 53))
(declare-const x FPN)
(declare-const y FPN)
(declare-const z FPN)
(declare-const q FPN)
(declare-const mpfx FPN)

(assert (= mpfx (fp.fma roundTowardNegative
		  ((_ to_fp 11 53) roundNearestTiesToEven 1.743105131865309687100307201035320758819580078125 (- 885))
		  ((_ to_fp 11 53) roundNearestTiesToEven (- 1.9517798820926548497567409867770038545131683349609375) 845)
		  ((_ to_fp 11 53) roundNearestTiesToEven (- 1.8242957893466726915221443050540983676910400390625) (- 40)))))

(assert (= x ((_ to_fp 11 53) roundNearestTiesToEven 1.743105131865309687100307201035320758819580078125 (- 885))))
(assert (= y ((_ to_fp 11 53) roundNearestTiesToEven (- 1.9517798820926548497567409867770038545131683349609375) 845)))
(assert (= z ((_ to_fp 11 53) roundNearestTiesToEven (- 1.8242957893466726915221443050540983676910400390625) (- 40))))
(assert (= q (fp.fma roundTowardNegative x y z)))
(assert (not (= q mpfx)))

(check-sat)
(check-sat-using smt)
